A, B:Type, g:(A(B + Top)), X:MaInterface(A), es:ES.
ma-interface-consistent(es;X)  ma-interface-consistent(es;ma-interface-compose(g;X)) 

latex

Definitions	Type, x:AB(x), b, a:A fp B(a), MaInterface(T), x:A  B(x), ES, let x,y = A in B(x;y), ma-interface-consistent-at(es;i;X), Atom$n, Id, t  T, Void, x:A.B(x), Top, Knd, {x:A| B(x)} , State(ds), left + right, x:A. B(x), P  Q, x.A(x), hasloc(k;i), x. t(x), True, T, x  dom(f), ma-interface-consistent(es;X), ma-interface-compose(g;X), P  Q, P & Q, P  Q, g o f, IdDeq
Lemmas	ma-interface-consistent-at-compose, ma-interface-compose wf, fpf-dom wf, subtype-fpf2, Id wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf